the_w:World, l:IdLnk, t:. queue(l;t)  {m:Msg| mlnk(m) = l } List 

latex

Definitions	x:A. B(x), t  T, queue(l;t), mlnk(m), 1of(t), snds(l;t), m(l;t), onlnk(l;mss), , S  T, Msg, Msg(M), x. t(x), {i..j}, i  j < k, P & Q, Prop, P  Q, x(s), P  Q
Lemmas	nth tl wf, w-Msg wf, IdLnk wf, length wf1, w-action wf, ldst wf, w-rcvs wf, nat wf, world wf, concat wf, map wf, int seg wf, upto wf, filter type, eq lnk wf, w-m wf, lsrc wf, le wf, Msg wf, w-M wf, Id wf, mlnk wf, subtype rel list, assert wf, pi1 wf, assert-eq-lnk